\begin{tabbing}
$\forall$\=$i$:Id, $k$:Knd, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Type,\+
\\[0ex]$f$:((${\it tg}$:Id $\times$ (State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$(${\it da}$(rcv($l$,${\it tg}$))?Void List))) List).
\-\\[0ex](source($l$) = $i$)
\\[0ex]$\Rightarrow$ \=@$i$: with declarations \+
\\[0ex]ds:${\it ds}$
\\[0ex]d\=a:${\it da}$\+
\\[0ex]$k$(v) sends $f$ s v on link $l$ 
\-\\[0ex]realizes ${\it es}$.
\\[0ex](($\forall$$x$:Id. vartype($i$;$x$) $\subseteq$r ${\it ds}$($x$)?Top)
\\[0ex]\& ($\forall$$e$:E. (loc($e$) = $i$ $\in$ Id) $\Rightarrow$ (valtype($e$) $\subseteq$r Valtype(${\it da}$;kind($e$))))
\\[0ex]\& ($\forall$$e$:E. ($\uparrow$isrcv($e$)) $\Rightarrow$ (lnk($e$) = $l$ $\in$ IdLnk) $\Rightarrow$ (valtype($e$) $\subseteq$r Valtype(${\it da}$;kind($e$))))
\\[0ex]\& (\{$m$:Msg$\mid$ source(mlnk($m$)) = $i$\}  $\subseteq$r Msg($\lambda$$l$,${\it tg}$. ${\it da}$(rcv($l$,${\it tg}$))?Top)))
\\[0ex]c$\wedge$ \=($\forall$$e$:E.\+
\\[0ex](loc($e$) = $i$ $\in$ Id)
\\[0ex]$\Rightarrow$ (kind($e$) = $k$ $\in$ Knd)
\\[0ex]$\Rightarrow$ (\=sends($l$;$e$)\+
\\[0ex]=
\\[0ex]tagged{-}messages($l$;$\lambda$$z$.$z$ when $e$;val($e$);$f$)
\\[0ex]$\in$ (Msg($\lambda$$l$,${\it tg}$. ${\it da}$(rcv($l$,${\it tg}$))?Top) List)))
\-\-\-
\end{tabbing}